(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(assert (xor v12 v3 v1 v1))
(push)
(assert v13)
(declare-const v15 Bool)
(assert v5)
(declare-const v16 Bool)
(declare-const v17 Bool)
(push)
(declare-const _12-0 (_ BitVec 12))
(assert (distinct v10 (= v15 v3 v10 v2 v6 v17 v9 v3 v6) v13 (= _12-0 _12-0 _12-0 _12-0 _12-0)))
(declare-const v19 Bool)
(assert v3)
(assert (distinct v19 v6 v17 (or v16 v7 v5 v8 v3 (xor v12 v3 v1 v1)) (xor v12 v3 v1 v1)))
(check-sat)
